/*
STATIC ALLOY - SOFTWARE ENGINEER II

Group: 						Mersede Sadeghi and Samuele Tosatto
Project reference:  	DreamTravel
*/

sig BasicProduct{
	hasProvider: one Provider,
}

sig StandardPackage{
	//Product that compose the package
	product: some BasicProduct,
	//Product to suggest in one package
	suggestedProduct: set BasicProduct,
}{
	product & suggestedProduct = none 
}

sig RealProduct{
	hasPeople : some People,
	generatedFrom : one BasicProduct,
}

sig PersonalizedPackage{
	product: some RealProduct,
	generatedFrom : one StandardPackage,
	payment: set Payment,
}

sig User{

}

sig Customer extends User{
	hasPackage: set PersonalizedPackage,
	hasPeople: some People,
}

sig Employee extends User{
	
}

sig Provider{

}

sig Invitation{
	sender: one Customer,
	receiver: some Customer,
	package: one PersonalizedPackage,
	
}{
	//there are no sender that invite himself
	no s:sender{
 		s in receiver
	}
	//the package has to be owned by the sender (*and not by any receiver*)
	some p:package{
		p in sender.hasPackage and
		all  r:receiver{
			not (p in r.hasPackage)
		}
	}
}



sig People{

}

sig Payment{
	customer : one Customer,
}


//A customer cannot be invited two times to the same package
fact NoDuplicateInvitaion{
	all i1 : Invitation {
		all i2 : Invitation{
			i1!=i2 and i1.package = i2.package implies (
				(i1.receiver & i2.receiver) = none
			)
		} 
	}
}

//There are no customer with people in common
fact NoPeopleInCommon{
	all c1:Customer, c2:Customer{
		c1!=c2 implies (
			c1.hasPeople & c2.hasPeople = none
		)
	}
}

//There are no personalized package without a customer 
fact NoPersonalizedWithoutCustomer{
	all p:PersonalizedPackage{
		some c:Customer{
			p in c.hasPackage
		}
	}
}

//If a product "contains" a people, that people has to be "owned" by a customer that "owns" the package
fact PeopleAndCustomerAndPackage{
	all pck :PersonalizedPackage{
		all pr : pck.product{
			all pe : pr.hasPeople{
				some c : Customer {
					pck in c.hasPackage and
						pe in c.hasPeople
				}
			}
		}
	}
	
}

//A real product is contained not in more than one package 
fact NoSharedProduct{
	all p1:PersonalizedPackage{
		all p2:PersonalizedPackage{
			p1!=p2 implies p1.product & p2.product = none
		}
	}
}

//All real product has to been contained in at least one package
fact ProductOnePackage{
	all p:RealProduct{
		some pa:PersonalizedPackage{
			p in pa.product
		}
	}
}

// If realProdoct1 is In PersonalaizedPackage1 -> basicProduc of the real product
// belong to standardPackage1  of the personalized package
fact RealProductIsCorrectly{
	all p:PersonalizedPackage{
		all r:p.product{
			r.generatedFrom in p.generatedFrom.product or
			r.generatedFrom in p.generatedFrom.suggestedProduct
		}
	}
}

//A payment on a package can be done by a customer from that package
fact PaymentConsistency{
	all p:Payment{
		some pck:PersonalizedPackage{
			p in pck.payment and
			pck in p.customer.hasPackage
		}
	}
}

//Check that there are no payment for one package made by the same customer
fact PaymentConsistency2{
	all p: PersonalizedPackage{
		 all p1: p.payment{
			all p2:p.payment{
				p1!=p2 implies p1.customer!=p2.customer	
			}	
		}
	}
}

//For each payment there are no more than 1 package
fact PaymentNoShared{
		all p1: PersonalizedPackage{
			all p2: PersonalizedPackage{
				p1!=p2 implies p1.payment & p2.payment = none
			}
		}
}
pred show(){
}

run show




